\documentclass[a4paper,10pt]{article}

%%\input{../sty/base}

\usepackage[ruled,vlined,linesnumbered,french]{algorithm2e}


\newcommand*{\titleAT}{\begingroup%
\drop=0.1\textheight
\vspace*{\drop}
\rule{\textwidth}{1pt}\par
\vspace{2pt}\vspace{-\baselineskip}
\rule{\textwidth}{0.4pt}\par
\vspace{0.5\drop}
\centering

{\Huge THE BOOK}\\[0.5\baselineskip]
{\Large OF}\\[0.75\baselineskip]
{\Huge CONUNDRUMS}\par
\vspace{0.25\drop}
\rule{0.3\textwidth}{0.4pt}\par
\vspace{\drop}
{\Large \scshape The Author}\par
\vfill
{\large \textcolor{Medium}{\plogo}}\\[0.5\baselineskip]
{\large\scshape the publisher}\par
\vspace*{\drop}
\endgroup}





%opening
\title{MUC Detection by using iterative method}
\author{HU Jun}

\newcommand{\HRule}{\rule[3mm]{\textwidth}{0.5mm}}
\begin{document}

\begin{minipage}{\textwidth}
\HRule \\
\noindent\ignorespaces \textbf{Technical Report}
\maketitle
\end{minipage}

% \titleAT


%%\selectlanguage{english}
\begin{abstract}
In this paper, we introduce a iterative method to extract the Minimum Unsatisfiable Core in CSP. By using an iterative enforced exact method, we are trying to extract minimum unsatisfaction core in CSP. 
\end{abstract}


\section{Introduction}
Recently, CSP researchers are focus on finding Minimum Unsatisfaction Core in over-constrained CSP. Many methods are inspirated from SAT. As the constraints in CSP are very different from those in SAT, some SAT methods couldn't be well adapted in CSP. 

% Etat de l'art sur la problèmatique de MUC


\subsection{Over-constrained CSP}
In real world instances, there is always over-constrained CSP. The objectif is to find 


\subsection{Minimum Unsatisfiable Core}
Unsatisfiable cores in CSP are composed by several inconsisted variables. As in SAT, several inconsisted variables are stringed by clauses. A unsatisfiable core called MUC, if it becomes satisfiable by removing only one variable from the core. 



\section{Method - EDBT}
Based on DBT, 

\begin{algorithm}
\Donnees{une liste de variables}
\Tq{Ce n'est pas la fin de la liste}{
	Affecter la variable courante\;
	\Si{il est DeadEnd}{
		\Si{Trouver la variable conflit}{
			desinstancier la variable conflit\;
			variable courante $\leftarrow$ variable conflit\;
			continuer\;
		}\Sinon{
			\Si{il y a des variables non visites}{
				variable courante $\leftarrow$ variable non-visite\;
				continuer\;
			}\Sinon{
				\Sortie{les variables sur lesquelles le probleme est non realisable}
			}
		}
		
	}\Sinon{
		variable courante $\leftarrow$ variable suivante\;
	}
}
\Res{une solution realisable}
\caption{Algorithme EDBT}
\end{algorithm}















\subsection{Heuristic proposed to accelarate the process}
As an exact method, EDBT is born with the defaults. 


%In over-constrained CSP problem, there is always request for extracting the minimum unsatisfaction core. 

\section{Conclusion}



\end{document}
